4.1. 函数🔗

Lean 内建支持函数类型。函数将一个类型的值（称为 定义域）映射到另一个类型的值（称为陪域），而 函数类型 用于指定函数的定义域与陪域。

函数类型有两种形式：

依值: 依值函数类型会显式命名参数，并允许函数的陪域类型显式地引用该名称。由于类型可以依赖于值，依值函数可根据输入参数返回不同类型的值。依值函数有时也被称为 依值积，因为它们对应于集合的索引积。
非依值: 非依值函数类型不会为参数命名，并且陪域类型不依赖于具体参数。

依值函数类型

函数 two 根据传入参数的不同，返回不同类型的值：

def two : (b : Bool) → if b then Unit × Unit else String :=
  fun b =>
    match b with
    | true => ((), ())
    | false => "two"

函数体不能直接用 if...then...else... 写出，因为它不会像 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not.match 那样细化类型。

在 Lean 的核心语言中，所有函数类型实际上都是依值的：非依值函数类型只是参数名未出现在陪域中的依值函数类型而已。此外，只要名称变换后一致，使用不同参数名的两个依值函数类型可以是定义等价的。不过，Lean 的繁释器不会为非依值函数的参数引入局部绑定。

依值函数与非依值函数的定义等价性

类型 (x : Nat) → String 和 Nat → String 是定义等价的：

example : ((x : Nat) → String) = (Nat → String) := rfl

同样，类型 (n : Nat) → n + 1 = 1 + n 和 (k : Nat) → k + 1 = 1 + k 也是定义等价的：

example : ((n : Nat) → n + 1 = 1 + n) = ((k : Nat) → k + 1 = 1 + k) := rfl

非依值函数不会绑定变量

下述关于“数组所有元素均非零”的定义需要依值函数：

def AllNonZero (xs : Array Nat) : Prop :=
  (i : Nat) → (lt : i < xs.size) → xs[i] ≠ 0

这是因为繁释器对于数组访问需要传入一个下标不越界的证明。非依值的版本则不会引入这个已知条件：

def AllNonZero (xs : Array Nat) : Prop :=
  (i : Nat) → (i < xs.size) → failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
xs : Array Nat
i : Nat
⊢ i < xs.sizexs[i] ≠ 0

failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
xs : Array Nat
i : Nat
⊢ i < xs.size

虽然核心类型理论没有隐式参数功能，函数类型仍可记录参数是否为隐式。这一属性仅被 Lean 的繁释器利用，对核心的类型检查和定义等价完全无影响，因此思考核心理论时可以忽略这一信息。

隐式和显式函数类型的定义等价性

即使一个参数是隐式、另一个是显式，类型 {α : Type} → (x : α) → α 和 (α : Type) → (x : α) → α 也是定义等价的。

example :
    ({α : Type} → (x : α) → α)
    =
    ((α : Type) → (x : α) → α)
  := rfl

4.1.1. 函数抽象🔗

在 Lean 的类型理论中，函数是通过 函数抽象 来创建的，它会绑定一个变量。在某些社区里，这一概念又被称为 λ 表达式（lambda）（源于 Alonzo Church 的记号），或 匿名函数（因其无需在全局环境中指定名称）。应用函数时，Lean 通过 β-规约，用实参替换被绑定的变量。在编译代码时，这是严格发生的——参数须先被求值为值。类型检查阶段则没有这样的限制，定义等价的等式理论允许对任意项做 β-规约。

在 Lean 的项语言中，函数抽象可以接收多个参数或在参数位置用模式匹配。这些高级特性会被翻译为底层核心语言中的简单操作，核心语言中每次函数抽象严格只接收一个参数。此外，并非所有函数都由函数抽象构建：类型构造子、构造子、递归子都可能拥有函数类型，但不能仅通过函数抽象定义。

4.1.2. 柯里化🔗

在 Lean 的核心类型理论中，每个函数都仅将定义域的每一个元素映射到陪域的单个元素。换言之，函数实际上只接受一个参数。多参数函数实现时，实际上是通过定义高阶函数——先接收第一个参数，返回一个新函数，该新函数再接收剩余参数。这样的编码方式称为 柯里化，此术语由并以 Haskell B. Curry 命名、推广。 Lean 提供的函数定义、类型声明与应用语法表现为多参数函数，但繁释之后的本质都是只带一个参数的函数抽象。

4.1.3. 外延性🔗

Lean 中函数的定义等价是 内涵性的。也就是说，定义等价的判定本质是基于语法的（仅考虑绑定变量的重命名及规约）。粗略而言，只有当两个函数本质上实现了“同一算法”时，才被认为定义等价；而数学上通常的函数相等——即若它们对所有相同输入都有相同输出——则不一定如此。

定义等价是类型检查器赖以工作的基础，因此需要可预测性。内涵等价中的语法特征，使得验证算法容易形式化；而若要求外延等价则意味着答案可能要靠证明任意的函数相等性定理，无法提出规范的检查算法，因此不适合作为类型检查依据。函数的外延性被设计为一种可供推理用的原则——可在证明两个函数相等的命题时调用。

除了规约与绑定变量重命名外，Lean 的定义等价还支持一种特殊形式的外延性，即 η-等价：一个函数与“把它作用于参数后返回”的函数抽象定义等价。对于 (x : α) → β x 类型的 f，f 与 fun x => f x 是定义等价的。

在函数推理时，可以使用定理 funext与某些内涵型理论不同，funext 在 Lean 中是一个定理，可以通过商类型证明，或相关的 funext 和 ext 策略，证明两个函数仅当对所有输入映射结果相等时亦相等。

theorem

funext.{u, v} {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
  (h : ∀ (x : α), f x = g x) : f = g
funext.{u, v} {α : Sort u}
  {β : α → Sort v} {f g : (x : α) → β x}
  (h : ∀ (x : α), f x = g x) : f = g

**函数外延性。**如果两个函数对所有可能的参数都返回相等的结果，那么它们就是相等的。

它被称为“外延性”，因为它提供了一种基于基础数学函数的性质，而不是基于用于表示它们的语法，来证明两个对象相等的方法。函数外延性是一个可以用商类型证明的定理。

4.1.4. 完全性与终止性🔗

Lean 支持用 Lean.Parser.Command.declaration : commanddef 来递归定义函数。从 Lean 逻辑的角度看，所有函数都是完全的：即每个定义域元素都能在有限步之内映射为陪域的某个元素。某些编程语言社区对“完全”的定义略有不同，仅要求不因未覆盖所有可能而崩溃，允许不终止。完全函数对所有类型正确参数都有定义，并且不会因模式匹配遗漏或无限递归而导致崩溃或无终止。

尽管 Lean 的逻辑模型要求函数完全，Lean 作为实用编程语言也提供了若干“逃生口”：那些未被证明终止的函数，只要其陪域被证明是非空的，也可用于 Lean 的逻辑中。此类函数逻辑层面会被视作“未解释函数”，其计算行为在推理中被忽略；但在编译后照常可被调用。还有些函数被标记为 unsafe，不可用于 Lean 逻辑。有关递归函数的更多细节，见偏函数和 unsafe 函数定义小节。

同理，某些编译期可运行失败的操作（如数组越界访问）在已知结果类型 inhabitable（可被占用）时可以正常使用。此时，逻辑层面这些操作会返回一个任意选定的该类型 inhabitant（具体是类型 Inhabited 实例指定的值）。

崩溃示例

函数 thirdChar 提取数组第三个元素，若数组太短则“崩溃”返回默认值：

def thirdChar (xs : Array Char) : Char := xs[2]!

对于 #['!'] 和 #['-', 'x'] 这种原本没第三个元素的数组，返回“第三个元素”其实等价——都为任意字符：

example : thirdChar #['!'] = thirdChar #['-', 'x'] := rfl

实际上，基于 Char 的默认实现，这两个都等于 'A'：

example : thirdChar #['!'] = 'A' := rfl
example : thirdChar #['-', 'x'] = 'A' := rfl

4.1.5. API 参考🔗

Function 命名空间下提供了丰富的泛用函数操作工具。

def

Function.comp.{u, v, w} {α : Sort u} {β : Sort v} {δ : Sort w}
  (f : β → δ) (g : α → β) : α → δ
Function.comp.{u, v, w} {α : Sort u}
  {β : Sort v} {δ : Sort w} (f : β → δ)
  (g : α → β) : α → δ

函数组合，通常用中缀运算符∘表示。通过组合两个已存在的函数创建一个新函数，其中一个函数的输出用作另一个函数的输入。

例子:

Function.comp List.reverse (List.drop 2) [3, 2, 4, 1] = [1, 4]
(List.reverse ∘ List.drop 2) [3, 2, 4, 1] = [1, 4]

def

Function.const.{u, v} {α : Sort u} (β : Sort v) (a : α) : β → α
Function.const.{u, v} {α : Sort u}
  (β : Sort v) (a : α) : β → α

常函数会忽略其参数。

如果a : α，那么Function.const β a : β → α就是“值为a的常函数”。对所有参数b : β，Function.const β a b = a。

示例:

Function.const Bool 10 true = 10
Function.const Bool 10 false = 10
Function.const String 10 "any string" = 10

def

Function.curry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2}
  {φ : Sort u_3} : (α × β → φ) → α → β → φ
Function.curry.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {φ : Sort u_3} : (α × β → φ) → α → β → φ

将一个接受一对参数的函数转换为等效的双参数函数。

例如:

Function.curry (fun (x, y) => x + y) 3 5 = 8
Function.curry Prod.swap 3 "five" = ("five", 3)

def

Function.uncurry.{u_1, u_2, u_3} {α : Type u_1} {β : Type u_2}
  {φ : Sort u_3} : (α → β → φ) → α × β → φ
Function.uncurry.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {φ : Sort u_3} : (α → β → φ) → α × β → φ

将一个带有两个参数的函数转换为一个接受参数对的等价函数。

例如:

Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]
[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]